Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Uniqueness of adjunction data #131

Merged
merged 12 commits into from
Oct 27, 2023
Merged

Uniqueness of adjunction data #131

merged 12 commits into from
Oct 27, 2023

Conversation

emilyriehl
Copy link
Collaborator

@emilyriehl emilyriehl commented Oct 22, 2023

This essentially proves that given a functor u : B -> A from a Rezk type to a Segal type, the question of whether u admits a left adjoint is a proposition.

Following RS 11.23 the strategy is to prove that the type of pairs (fa, ηa) defining a transposition equivalence hom B fa b -> hom A a (u b) is a proposition.

Thus pull request stops with a proof identifying two such pairs (fa, ηa) = (fa', ηa'). To finish I need a proof that is-equiv is a property so I'll wait for @floverity to finish with issues #56.

I added a few auxiliary functions along the way, in particular reversed versions of various complicated paths, which I called rev-name-of-original-path. I noticed in at least one instance in the library we've denoted this by name-of-original-path' so let me know if that is preferred.

@emilyriehl
Copy link
Collaborator Author

I'm a little rusty with formalization so feel free to take time reviewing this. In the meanwhile, I'll help with some of the open PRs!

@emilyriehl
Copy link
Collaborator Author

About to board a plane again. I'm going to work on switching the code over to the new style guide in progress.

@emilyriehl
Copy link
Collaborator Author

This and #132 are now ready for review.

Copy link
Member

@fizruk fizruk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me!

I would say one thing though: there are many definitions without any supplementary text (explanation/motivation/structural comments). That said, I'm not ready to advise on specific text to add here.

@emilyriehl
Copy link
Collaborator Author

Good point @fizruk. Once I've actually completed of the proof of the theorem (waiting on some open issues to be finished first) I'll submit another PR with better commenting. But I'll merge this version now.

@emilyriehl emilyriehl merged commit 5017767 into main Oct 27, 2023
2 checks passed
@emilyriehl emilyriehl deleted the more-adjunctions branch October 27, 2023 17:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants